<!doctype html>
<html lang="en">
  <head>
    <!-- Required meta tags -->
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">

    <!-- Bootstrap CSS -->
	<!--<link rel="stylesheet" href="css/bootstrap.min.css" >-->
	<link rel="stylesheet" href="https://leanprover-community.github.io//css/lean.css" >
	<link rel="stylesheet"
          href="https://fonts.googleapis.com/css?family=Merriweather:700">
    

	<script>
                function buildShortcutsForStructures(names) { 
                        const o = {}
                        names.forEach(name => o[name] = `\\mathbb\{${name}\}`)
                        return o
                }
		MathJax = {
			  tex: {
                                  macros: {
                                          ...buildShortcutsForStructures(["R", "Q", "Z", "N", "C"]),
                                  },
				      inlineMath: [['$', '$'], ['\\(', '\\)']]
				    },
		};
	</script>
	<script type="text/javascript" id="MathJax-script" async
		  src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js">
	</script>

	<title>Learning Lean</title>
  </head>
  <body>
  <div id="wrapper">
  <nav class="navbar navbar-expand-lg navbar-light bg-gradient-light">
    <div class="d-flex flex-grow-1">
		<a class="navbar-brand" href="https://leanprover-community.github.io/index.html">Lean Community
    </a>
    </div>

    <button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation">
      <span class="navbar-toggler-icon"></span>
    </button>
    <div class="collapse navbar-collapse flex-grow-1 text-right" id="navbarSupportedContent">
      <ul class="navbar-nav ml-auto">
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Try it!
          </a>
		  <div class="dropdown-menu " aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/lean-web-editor">Lean online</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/get_started.html">Install</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Learn
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/learn.html">Resources</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.github.io/theorem_proving_in_lean/">Theorem proving in Lean</a>
			
			
			
			<a class="dropdown-item" href="http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/">The natural number game</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib-overview.html">Library overview</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib_docs">API documentation</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Community
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html">Meet us</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.zulipchat.com/">Zulip chat</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html#maintainers">Maintainers</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/contribute/index.html">How to contribute</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/papers.html">Papers</a>
			
			
          </div>
        </li>
		
      </ul>
    </div>
  </nav>
  <div class="container-sm mt-4">
	  
<h1 id="learning-lean" class="markdown-heading">Learning Lean <a class="hover-link" href="#learning-lean">#</a></h1>
<p>There are many ways to start learning Lean, depending on your background and
taste. They are all fun and rewarding, but also difficult and
occasionally frustrating. Proof assistants are still difficult to use,
and you cannot expect to become proficient after one afternoon of
learning.</p>
<h2 id="hands-on-approaches" class="markdown-heading">Hands-on approaches <a class="hover-link" href="#hands-on-approaches">#</a></h2>
<ul>
<li>
<p>Whatever your background, if you want to dive right away, you can play the
<a href="http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/">Natural Number Game</a>
by Kevin Buzzard and Mohammad Pedramfar. This is a online interactive tutorial to Lean
focused on proving properties of the elementary operations on natural numbers.</p>
</li>
<li>
<p>For a faster paced and broader dive, you can get the
<a href="https://github.com/leanprover-community/tutorials">tutorials project</a>.
(You already have it if you installed an autonomous bundle or
followed the instructions on <a href="install/project.html">this page</a>.)
This tutorial is specifically geared towards mathematics rather than
computer science. The last files of this project are easier if you have
already encountered the definition of limits of sequences of real
numbers.</p>
</li>
<li>
<p>A brand new resource that is still under construction is
<em>Mathematics in Lean</em>.
It can be <a href="https://leanprover-community.github.io/mathematics_in_lean/">read online</a>,
or downloaded <a href="https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf">as a pdf</a>,
but it is really meant to be used in VSCode, doing exercises
on the fly (see the <a href="https://leanprover-community.github.io/mathematics_in_lean/introduction.html#getting-started">instructions</a>).
It currently covers roughly the same ground as the tutorials prooject.</p>
</li>
<li>
<p>Once you know the basics, you can also learn by solving Lean puzzles
on <a href="https://www.codewars.com/?language=lean">Codewars</a>.</p>
</li>
</ul>
<p>Whatever resource you choose to use from the above list, it could
be useful to have a copy of our <a href="https://leanprover-community.github.io//img/lean-tactics.pdf">tactic cheat sheet</a>
at hand, for reference.</p>
<h2 id="textbooks" class="markdown-heading">Textbooks <a class="hover-link" href="#textbooks">#</a></h2>
<ul>
<li>
<p>If you prefer reading a book (with exercises), the standard reference is
<a href="https://leanprover.github.io/theorem_proving_in_lean/">Theorem Proving in Lean</a>.
You almost certainly want to read it at some point anyway, since it
explains foundational things much better than any hands-on tutorial
could do.</p>
</li>
<li>
<p>If you are very new to the concept of logic and proofs, you can read
<a href="https://leanprover.github.io/logic_and_proof/">Logic and Proof</a>,
a textbook that is a first rigorous proving course that teaches Lean at the same time.</p>
</li>
<li>
<p>If you have a computer science background, and are primarily interested
in software verification, then you can read
<a href="https://github.com/blanchette/logical_verification_2020/raw/master/hitchhikers_guide.pdf">The Hitchhiker's Guide to Logical Verification (pdf)</a>,
course notes for an <a href="https://lean-forward.github.io/logical-verification/2020/index.html">MSc-level course</a> at VU Amsterdam.</p>
</li>
<li>
<p>If you want a systematic exposition of syntax and commands, then you
can read the <a href="https://leanprover.github.io/reference/">reference manual</a>.</p>
</li>
</ul>
<h2 id="miscellaneous-topics" class="markdown-heading">Miscellaneous topics <a class="hover-link" href="#miscellaneous-topics">#</a></h2>
<p>In addition to the above sources, we have a number of small documents
covering specific topics:</p>
<ul>
<li>The <a href="extras/conv.html">conversion tactic mode</a></li>
<li>The <a href="extras/simp.html">simplifier</a></li>
<li>The <a href="extras/calc.html">calc environment</a></li>
<li><a href="extras/well_founded_recursion.html">Well founded recursion</a></li>
</ul>
<h2 id="metaprogramming-and-tactic-writing" class="markdown-heading">Metaprogramming and tactic writing <a class="hover-link" href="#metaprogramming-and-tactic-writing">#</a></h2>
<p>After using Lean for a while, you may want to learn how to write your
own tactics. This is less documented than proof writing, but you can
still have a look at the following resources.</p>
<ul>
<li>The <a href="extras/tactic_writing.html">tactic writing tutorial</a>
covers the basics and enables you to read more advanced sources, for instance
the code of
<a href="https://leanprover-community.github.io/mathlib_docs/tactics.html">existing tactics</a>.</li>
<li><a href="https://github.com/blanchette/logical_verification_2020/raw/master/hitchhikers_guide.pdf">The Hitchhiker's Guide to Logical Verification (pdf)</a> also has a chapter on metaprogramming.</li>
<li>The reference paper on
<a href="https://leanprover.github.io/papers/tactic.pdf">Lean metaprogramming</a>.</li>
</ul>
<h2 id="more-on-foundations" class="markdown-heading">More on foundations <a class="hover-link" href="#more-on-foundations">#</a></h2>
<p>If you are interested in foundations of Lean, you can first read a
very rough sketch
<a href="https://leanprover-community.github.io/lean-perfectoid-spaces/type_theory.html">here</a>.
If you want a bit more detail, you can read the first chapter
of the <a href="https://homotopytypetheory.org/book/">HoTT book</a>, ignoring
anything where univalence is mentioned.</p>
<p>Another potentially useful resource is
<a href="https://coq.github.io/doc/master/refman/language/cic.html">this page</a>
from Coq's documentation. The foundations of Coq are very very close to
those of Lean. The most relevant differences to keep in mind are:</p>
<ul>
<li>Lean's <code>Prop</code> is proof-irrelevant, so it is closer to <code>SProp</code> from the
page above.</li>
<li>Universes in Lean are <em>not</em> cumulative. However, any type can be lifted
to higher universes.</li>
<li>Lean natively supports quotient types and their associated reduction
rule (see <a href="https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#quotients">this
section</a>
of <em>Theorem proving in Lean</em>).</li>
</ul>
<p>If you can read the above Coq documentation then you are ready for
<a href="https://github.com/digama0/lean-type-theory/releases">this paper</a> by
Mario Carneiro which precisely describes the type theory of Lean.</p>
<p>Note that understanding type theoretic foundations is not at all necessary
to use Lean.</p>

  </div>
</div>

  <nav class="footer navbar navbar-expand-lg navbar-light bg-light justify-content-end">
  <ul class="nav">
    <li class="nav-item">
      <a class="nav-link active" href="https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/learn.md">Suggest edits to this page on GitHub</a>
    </li>
  </ul>
</nav>

    <script src="https://code.jquery.com/jquery-3.4.1.slim.min.js" integrity="sha384-J6qa4849blE2+poT4WnyKhv5vZF5SrPo0iEjwBvKU7imGFAV0wwj1yYfoRSJoZ+n" crossorigin="anonymous"></script>
    <script src="https://leanprover-community.github.io//js/bootstrap.min.js"></script>
    
  </body>
</html>